## Tseitin transformation

Let $F$ be a formula in $\text{conjunctive normal form}$ (CNF), i.e., a conjunction of clauses

$$
\bigwedge\limits_i^{C} \bigvee\limits_j^{S_i} \ell_{i,j},\ \text{where}\ \ell_{i,j} \in \{ P, \neg P \mid P \text{ is an atom} \}
$$ {#eq:clauses}

Note that every clause $C_i$ with $m$ literals can be seen as a "nested" disjunction, i.e.,

$$
C_i = (\ell_{i,1} \lor (\ell_{i,2} \lor (\text{...} \lor (\ell_{i,m-1} \lor \ell_{i,m})
$$ {#eq:nested}

Explain how you can use Tseitin's transformation to convert any arbitrary formula in CNF into an ***equi-satisfiable*** formula in CNF whose clauses have at most 3 literals.

#### solution

A clause in the formula is with no loss of generality described by

$$
C_i = (\ell_{i,1} \lor \ell_{i,2} \lor (\ell_{i,3} \lor (\ell_{i,4} \lor (F))),\ F = \bigvee_{j}^A \ell_{i,j},\ A = {S_i} \setminus \{1,2,3,4\}
$$ {#eq:general-formula}

We can introduce a new symbol for a satisfiability-equivalent formula

$$
(\ell_{i,1} \lor \ell_{i,2} \lor O_1) \land (O_1 \Leftrightarrow (\ell_{i,3} \lor (\ell_{i,4} \lor (F)))
$$ {#eq:equivalent-formula}

and apply the corresponding Tseitin Encoding

$$
\begin{aligned}
(\ell_{i,1} \lor \ell_{i,2} \lor O_1)\land (\neg \ell_{i,3} \lor O_1) &\land \overbrace{(\neg(\ell_{i,4} \lor F) \lor O_1)}^{C_{i,const}} \\
&\land \underbrace{(\neg O_1 \lor \ell_{i,3} \lor (\ell{i,4} \lor (F)))}_{C_i,recursive}
\end{aligned}
$$ {#eq:tseitin}

Doing so yields two components for which we have to show that they contain at most 3 literals. The first of which represents a constant blow-up of conjuncts

$$
\begin{aligned}
C_{i,const} &= \neg (\ell_{i,4} \lor F) \lor O_1 \\
&= (\neg \ell_{i,4} \land \neg F) \lor O_1 \\
&= (\neg \ell_{i,4} \lor O_1) \land (\neg F \lor O_1) \\
&= (\neg \ell_{i,4} \lor O_1) \land (\neg (\bigvee_j^A \ell_{i,j} ) \lor O_1) \\
&= (\neg \ell_{i,4} \lor O_1) \land ((\bigwedge_j^A \neg \ell_{i,j} ) \lor O_1) \\
&= (\neg \ell_{i,4} \lor O_1) \land (\bigwedge_j^A \neg \ell_{i,j} \lor O_1) \\
\end{aligned}
$$ {#eq:conjuncts}

Note that [@eq:conjuncts] makes entensive use of the distributivity of conjuncts and disjuncts to expand $C_{i,const}$ into sub-clauses that are short enough.

The other remaining clause is $C_{i,recursive}$, for which it remains to be shown that the formula is a disjunction with at most 3 literals. This term is the original expression $C_i$ without the disjuncts $\ell_{i,1}$ and $\ell_{i,2}$. The expansion described in [@eq:equivalent-formula] and [@eq:tseitin] can thus be applied again until all clauses have been reduced to form an equi-satisfiable formula in CNF whose clauses have at most 3 literals.
